| Definitions | AtomFree(T;x), a:A fp B(a), Knd, Type, KindDeq, AtomFree(d), MsgA, da(M), M.da(a), EqDecider(T), union-deq(A;B;a;b), sumdeq(a;b), sum-deq(A;B;a;b), IdLnkDeq, IdDeq, product-deq(A;B;a;b), proddeq(a;b), prod-deq(A;B;a;b), AtomDeq, atom-deq-aux, NatDeq, <a,b>, nat-deq-aux, f(a),  x dom(f). v=f(x)   P(x;v), type List, left+right, IdLnk, Id, x:A B(x), Atom,  , {x:A| B(x) },  , A B,  A, P Q, False, Void, a<b, #$n, x:A B(x), f(x)?z,  x.A(x), Top, x:A. B(x),  x. t(x), t T |